(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
plus(s(s(x)), y) →+ s(plus(x, s(y)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x / s(s(x))].
The result substitution is [y / s(y)].
(2) BOUNDS(n^1, INF)